\chapter{Behavioral Theory of \hocore}
\label{chap:bt}
\minitoc

This chapter develops the behavioral theory of \hocore.
In Section \ref{s:bism} a notion of strong bisimilarity for
\hocore is studied; such a notion it is unique in that it coincides with 
other sensible behavioral equivalences in the higher-order setting.
The most remarkable property of strong bisimilarity in \hocore is that it is \emph{decidable}.
Section \ref{s:barbed} analyzes the relationship between strong bisimilarity and
(asynchronous) barbed congruence.
Section \ref{s:axiom} introduces a sound and complete axiomatization of strong bisimilarity.
This axiomatization is then used to obtain an upper bound to the complexity of the bisimilarity
problem.
In Section \ref{s:static} it is shown that strong bisimilarity becoms undecidable
if at least four static restriction are added to the calculus.
Section \ref{s:exten} briefly analyzes the impact of some extensions to the language
on the decidability results.
Section \ref{s:bt-concl} concludes.


\section{Bisimilarity in \ahopi}\label{s:bism}
\input{lics-bisim}

\input{lics-axiom}

\section{Other Extensions}\label{s:exten}
\input{lics-sext}

\section{Concluding Remarks}\label{s:bt-concl}
\input{lics-concl}